(set-option :smt.arith.solver 4)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const i0 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v15 Bool)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Int)) (=> (>= q2 40) (=> q1 v13))))
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const v19 Bool)
(push 1)
(assert (exists ((q3 Int) (q4 Bool) (q5 Bool)) v3))
(pop 1)
(declare-const v20 Bool)
(declare-const v21 Bool)
(assert (forall ((q6 Bool) (q7 Int)) (=> (= i7 q7) (distinct v15 (distinct v7 v2 (>= 10 i13) (or v1 v8 v3 v14 (< 0 0) v7 v10 v1)) v3))))
(declare-const v22 Bool)
(declare-const v23 Bool)
(assert (forall ((q8 Int) (q9 Int)) v18))
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const i17 Int)
(declare-const v28 Bool)
(declare-const v29 Bool)
(push 1)
(declare-const v30 Bool)
(assert (or v24 v23 v15))
(assert (or v23 (= i11 746) v24))
(assert (or (and v8 v13 (not v1) v20 (= (or v1 v8 v3 v14 (< 0 0) v7 v10 v1) v10 (not v6) v13 v4 v5) v16 v4 (>= 10 i13) v18 v11) (and v8 v13 (not v1) v20 (= (or v1 v8 v3 v14 (< 0 0) v7 v10 v1) v10 (not v6) v13 v4 v5) v16 v4 (>= 10 i13) v18 v11) v24))
(assert (or v24 (or (distinct (>= 30 (abs i0)) v2 v24) v26 v22 (> i16 (- i3)) v3 v16 (= i11 746)) v15 v24 (or (distinct (>= 30 (abs i0)) v2 v24) v26 v22 (> i16 (- i3)) v3 v16 (= i11 746)) (= i11 746)))
(check-sat)
(exit)
